Групоид Инфинити открывает свой репозиторий Coq пакетов

С коком такая тема, что не все пакеты обновляются часто, никому не нужны FTC,
Category Theory, CoInduction свойтва на последних коках. Последний — 8.6 —
вышел в декабре 2016, а у всех пакетов в OPAM стоит жестко меньше 8.6. Они там
язык тактик поменяли, и улучшлили тайпчек вселенных.

Демонстрировать кому-то всю силу кока приходится на своем компе, и простых
инструкций взять и склонировать что-то для известных теорем нет. Более того, не
все теоремы есть в OPAM, много просто валяются на ftp серверах унивеситетов.

Поэтому в соответствии с парадигмой "Грабь и Воруй" я принял решение сделать
свой репозиторий пакетов под игидой Групоид Инфинити. Делаю я это для того,
чтобы крамсать код пакетов в (само)-образовательных целях и публикации статей
по основаниями математики с примерами кок-термов. Следите за сайтом Групоид
Инфинити, а также языком Infinity Language.

Итак, встречайте, кодовое название проекта "Вери Мас Сач Вау"
https://github.com/verimath Логотип тупо ноль — обозначает начальный уровень
Кунг-фу в Зависимой теории :-)

Хочу сделать максимальный smooth экспириенс для математиков и академии, чтобы
студенты могли очень просто начать разрабатывать на коке. Смешно, но даже
матерые коко-писатели из НАН не знают как накатить HoTT патчи и чекнуть
гомотопические теоремы.

Хочу, чтобы простая последовательность действий всегда позволяла запустить
любой наш репо на последнем коке. У чуваков культуры оформления вообще никакой,
какие-то перл скрипты, беш скрипты — представьте, что вы говорите математику на
виндовсе поставить перл и беш, чтобы у вас работали теоремы. Вообщем, я это все
повыбрасывал и оставил только coq_makefile. В репозиториях ничего кроме
коковских файлов нет и все собирается простой последовательностью команд:

$ brew install opam
$ opam install coq
$ git clone http://github.com/verimath/topology && cd topology
$ coq_makefile -f Make -o Makefile
$ make

Начал я с таких тем-репозиториев — все рабочие (только ftc wip):

1. topology — общая топология + лемма Цорна
2. co — первый коиндуктивный репл-шелл на коке
3. real — действительные числа, как коиндуктивные стримы цифр
4. termination — терминальная категорная семантика коиндуктивных стримов
5. set — теория множеств Тарского-Гротендика
6. interpreter — интерпретатор гомотопической теории
7. ftc — основная теорема анализа по предложению риалити хакера
8. lambda — нетипизированное лямбда исчисление как инициальный объект категории
экспоненциальных монад

Пакеты можно будет добавлять так:

$ opam repo add coq-released https://groupoid.space/opam

Делаем зависимые лямбда термы ближе к народу!